Nuprl Lemma : assert-eq-lnk 0,22
a, b:IdLnk. a = b  a = b 
latex

Definitionsa = b, b, eqof(d), x:A. B(x), IdLnkDeq, t  T, Prop, P  Q, P & Q, P  Q, P  Q, IdLnk
Lemmasidlnk-deq wf, eqof wf, assert wf, deq property, iff functionality wrt iff, IdLnk wf

origin